/*******************************************************************************
 * Assurance Contract Annex Plugin for OSATE
 * Copyright 2023 Carnegie Mellon University.
 * NO WARRANTY. THIS CARNEGIE MELLON UNIVERSITY AND SOFTWARE ENGINEERING INSTITUTE
 * MATERIAL IS FURNISHED ON AN "AS-IS" BASIS. CARNEGIE MELLON UNIVERSITY MAKES NO
 * WARRANTIES OF ANY KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT
 * NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE OR MERCHANTABILITY, EXCLUSIVITY, OR
 * RESULTS OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT MAKE
 * ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT
 * INFRINGEMENT.
 * Released under a BSD (SEI)-style license, please see license.txt or contact
 * permission@sei.cmu.edu for full terms.
 * [DISTRIBUTION STATEMENT A] This material has been approved for public release and
 * unlimited distribution.  Please see Copyright notice for non-US Government use and
 * distribution.
 * Carnegie Mellon® is registered in the U.S. Patent and Trademark Office by Carnegie
 * Mellon University.
 * This Software includes and/or makes use of the following Third-Party Software subject
 * to its own license:
 * 1. Z3 (https://github.com/Z3Prover/z3/blob/master/LICENSE.txt) Copyright Microsoft
 * Corporation.
 * 2. Eclipse (https://www.eclipse.org/legal/epl-2.0/) Copyright 2000, 2023 Eclipse
 * contributors and others.
 * DM23-0575
 *******************************************************************************/
/*
 * generated by Xtext 2.27.0
 */
package org.osate.contract.validation;

import java.util.List;
import java.util.Map;
import java.util.stream.Stream;

import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.util.EcoreUtil;
import org.eclipse.xtext.validation.Check;
import org.osate.aadl2.Aadl2Package;
import org.osate.aadl2.NamedElement;
import org.osate.contract.contract.Argument;
import org.osate.contract.contract.ArgumentAssumption;
import org.osate.contract.contract.ArgumentExpression;
import org.osate.contract.contract.Contract;
import org.osate.contract.contract.ContractAssumption;
import org.osate.contract.contract.ContractElement;
import org.osate.contract.contract.ContractPackage;
import org.osate.contract.contract.Guarantee;
import org.osate.contract.contract.IStringLiteral;
import org.osate.contract.contract.Lambda;
import org.osate.contract.contract.Query;
import org.osate.contract.contract.SingleParameter;
import org.osate.contract.contract.SingleValDeclaration;
import org.osate.contract.contract.TupleDeclaration;
import org.osate.contract.contract.TupleName;
import org.osate.contract.contract.TupleParameter;
import org.osate.contract.typing.validation.ContractTypeSystemValidator;

/**
 * This class contains custom validation rules.
 *
 * See https://www.eclipse.org/Xtext/documentation/303_runtime_concepts.html#validation
 */
public class ContractValidator extends ContractTypeSystemValidator {
	@Override
	protected boolean isResponsible(Map<Object, Object> context, EObject eObject) {
		return eObject.eClass().getEPackage() == ContractPackage.eINSTANCE;
	}

	@Check
	public void checkDuplicateName(NamedElement named) {
		var name = named.getName();
		var duplicateFound = false;
		for (var current = named.eContainer(); !duplicateFound && current != null; current = current.eContainer()) {
			if (current instanceof Contract contract) {
				duplicateFound = isAlreadyDeclaredInQueries(named, contract.getQueries());
			} else if (current instanceof TupleDeclaration tuple) {
				duplicateFound = isAlreadyDeclaredInTupleNames(named, tuple.getNames());
			} else if (current instanceof Lambda lambda && !EcoreUtil.isAncestor(lambda.getParameter(), named)) {
				if (lambda.getParameter() instanceof SingleParameter parameter) {
					duplicateFound = parameter.getName().equals(name);
				} else if (lambda.getParameter() instanceof TupleParameter parameter) {
					duplicateFound = parameter.getNames()
							.stream()
							.anyMatch(tupleName -> tupleName.getName().equals(name));
				}
				if (!duplicateFound) {
					duplicateFound = isAlreadyDeclaredInQueries(named, lambda.getQueries());
				}
			} else if (current instanceof TupleParameter tuple) {
				duplicateFound = isAlreadyDeclaredInTupleNames(named, tuple.getNames());
			}
		}
		if (duplicateFound) {
			error("'" + name + "' is already declared", Aadl2Package.eINSTANCE.getNamedElement_Name());
		}
	}

	@Check
	public void checkContractAssumption(ContractAssumption ca) {
		if (!(ca.getContract() instanceof Contract)) {
			error("Expecting name of a contract", ContractPackage.eINSTANCE.getContractAssumption_Contract());
		}
	}

	@Check
	public void checkArgumentAssumption(ArgumentAssumption aa) {
		if (!(aa.getArgument() instanceof Argument)) {
			error("Expecting name of an argument", ContractPackage.eINSTANCE.getArgumentAssumption_Argument());
		}
	}

	@Check
	public void checkArgumentExpression(ArgumentExpression e) {
		int i = 0;
		for (ContractElement c : e.getContracts()) {
			if (!(c instanceof Contract)) {
				error("Expecting name of a contract", ContractPackage.eINSTANCE.getArgumentExpression_Contracts(), i);
			}
			i++;
		}
		i = 0;
		for (ContractElement c : e.getArguments()) {
			if (!(c instanceof Argument)) {
				error("Expecting name of an argument", ContractPackage.eINSTANCE.getArgumentExpression_Arguments(), i);
			}
			i++;
		}
	}

	@Check
	public void checkGuarantee(Guarantee g) {
		var code = g.getCode();
		var source = code.getSource();
		if (source != null) {
			if (source.isBlank()) {
				error("Guarantee cannot be empty", ContractPackage.eINSTANCE.getGuarantee_Code());
			}
		}
		var inter = code.getInter();
		if (inter != null) {
			var p = inter.getParts();
			if (p.size() == 1 && p.get(0) instanceof IStringLiteral l && l.getValue().isBlank()) {
				error("Guarantee cannot be empty", ContractPackage.eINSTANCE.getGuarantee_Code());
			}
		}
	}

	private static boolean isAlreadyDeclaredInTupleNames(NamedElement named, List<TupleName> tupleNames) {
		return tupleNames.stream()
				.takeWhile(tupleName -> tupleName != named)
				.anyMatch(tupleName -> tupleName.getName().equals(named.getName()));
	}

	private static boolean isAlreadyDeclaredInQueries(NamedElement named, List<Query> queries) {
		return queries.stream().takeWhile(query -> !EcoreUtil.isAncestor(query, named)).flatMap(query -> {
			if (query instanceof SingleValDeclaration singleVal) {
				return Stream.of(singleVal);
			} else if (query instanceof TupleDeclaration tuple) {
				return tuple.getNames().stream();
			} else {
				return Stream.empty();
			}
		}).anyMatch(existingNamed -> existingNamed.getName().equals(named.getName()));
	}

}